Inference at * 1 1 1 
Iof proof for Lemma add functionality wrt le:



1. i2 : 
2. j2 : 
3. i2  j2
4. i1 : 
5. i1 < 0
6. j1:. ((i1+1)  j1)  ((i1+1+i2)  (j1+j2))
7. j1 : 
8. i1  j1
  (i1+i2)  (j1+j2) 

latex

 by (RA ((DTerm j1+1 6) 
CollapseTHENM (D (-1)))) 

latex

C.

Definitions

False, A, t  T, P  Q, A  B, x:A. B(x)